Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    f(f(f(a,b),c),x)  → f(b,f(a,f(c,f(b,x))))
2:    f(x,f(y,z))  → f(f(x,y),z)
There are 6 dependency pairs:
3:    F(f(f(a,b),c),x)  → F(b,f(a,f(c,f(b,x))))
4:    F(f(f(a,b),c),x)  → F(a,f(c,f(b,x)))
5:    F(f(f(a,b),c),x)  → F(c,f(b,x))
6:    F(f(f(a,b),c),x)  → F(b,x)
7:    F(x,f(y,z))  → F(f(x,y),z)
8:    F(x,f(y,z))  → F(x,y)
The approximated dependency graph contains one SCC: {3-8}.
Tyrolean Termination Tool  (0.47 seconds)   ---  May 3, 2006